r:Rng, b:, p, q:|r|. (when b. (p +r q)) = ((when b. p) +r (when b. q))  |r| 

latex

Definitions	x:A. B(x), x f y, IMonoid, t  T, |g|, *, r+gp, AbGrp, Group{i}, Mon, P & Q, Prop, 1of(t), 2of(t), when b. p
Lemmas	mon when thru op, add grp of rng wf b, monoid p wf, grp car wf, grp op wf, grp id wf, abgrp wf, rng wf